/*
 * ConflictAnalyzerFullSearchSpace.cuh
 *
 *  Created on: Sep 25, 2013
 *      Author: jaime
 */

#ifndef CONFLICTANALYZERFULLSEARCHSPACE_CUH_
#define CONFLICTANALYZERFULLSEARCHSPACE_CUH_

class ConflictAnalyzerFullSearchSpace : public ConflictAnalyzer{
public:
	__device__ ConflictAnalyzerFullSearchSpace(
			int number_of_variable,
			CUDAClauseVec * formula,
			VariablesStateHandler * handler,
			int max_implication_per_var,
			DecisionMaker * dec_maker
#ifdef ENABLE_STATISTICS
			,RuntimeStatistics * stats
#endif

	);

	__device__ void reset();
	__device__ int get_number_last_conflicts();
	__device__ sat_status propagate(Decision d);
		/**
		 * Backtracks the current implication graph to an specific decision level, removing
		 * vertices and edges that are smaller than the specified decision level.
		 * * Does NOT remove implications or decisions!
		 */
	//__device__ void backtrack_to(int decision_level);
#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
	__device__ sat_status set_assumptions(GPUVec<Lit> * assumptions);
#else
	__device__ sat_status set_assumptions(GPUStaticVec<Lit> * assumptions);
#endif
	__device__ void restart();
private:
	__device__ sat_status propagate_all_clauses(Decision d, Clause * & conflicting);

};

#endif /* CONFLICTANALYZERFULLSEARCHSPACE_CUH_ */
